PRISM
=====
Version: 4.5
Date: Wed Apr 01 10:13:36 UTC 2020
Hostname: cb4ac6bf600d
Memory limits: cudd=1g, java(heap)=2g
Type: CTMC
Modules: D_def Y_def Z_def CC_def XX_def EE_def
Variables: D Y Z CC XX EE
Generator: stamina.InfCTMCModelGenerator
Type: CTMC
========================================================================
Approximation<1> : kappa = 1.0E-6
========================================================================
---------------------------------------------------------------------
Building model...
Computing reachable states... 22 5168 states
5168 states
Reachable states exploration and model construction done in 1.914 secs.
Sorting reachable states list...
Time for model construction: 1.951 seconds.
Type: CTMC
States: 5168 (1 initial)
Transitions: 42949
---------------------------------------------------------------------
Verifying Lower Bound for change_state_min .....
---------------------------------------------------------------------
Model checking: "change_state_min": P=? [ F<=T ((EE>40&(!EE=-1))&(CC<20&(!CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 8.461 seconds.
Value in the initial state: 0.0
Time for model checking: 8.488 seconds.
Result: 0.0 (value in the initial state)
---------------------------------------------------------------------
Verifying Upper Bound for change_state_max .....
---------------------------------------------------------------------
Model checking: "change_state_max": P=? [ F<=T ((EE>40|(EE=-1))&(CC<20|(CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 8.69 seconds.
Value in the initial state: 0.0830190021399403
Time for model checking: 8.697 seconds.
Result: 0.0830190021399403 (value in the initial state)
========================================================================
Approximation<2> : kappa = 9.999999999999999E-10
========================================================================
---------------------------------------------------------------------
Building model...
Computing reachable states... 35656 37916 38691 39127 39597 39671 states
1 39671 states
Reachable states exploration and model construction done in 16.795 secs.
Sorting reachable states list...
Time for model construction: 16.869 seconds.
Type: CTMC
States: 39671 (1 initial)
Transitions: 361885
---------------------------------------------------------------------
Verifying Lower Bound for change_state_min .....
---------------------------------------------------------------------
Model checking: "change_state_min": P=? [ F<=T ((EE>40&(!EE=-1))&(CC<20&(!CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.287226595180127 x 2100.0 = 6903.1758498782665
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 136.466 seconds.
Value in the initial state: 0.05007058777924607
Time for model checking: 136.507 seconds.
Result: 0.05007058777924607 (value in the initial state)
---------------------------------------------------------------------
Verifying Upper Bound for change_state_max .....
---------------------------------------------------------------------
Model checking: "change_state_max": P=? [ F<=T ((EE>40|(EE=-1))&(CC<20|(CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.287226595180127 x 2100.0 = 6903.1758498782665
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 136.236 seconds.
Value in the initial state: 0.055952025386081815
Time for model checking: 136.253 seconds.
Result: 0.055952025386081815 (value in the initial state)
========================================================================
Approximation<3> : kappa = 9.999999999999998E-13
========================================================================
---------------------------------------------------------------------
Building model...
Computing reachable states... 98794 116902 119198 119267 states
1 119267 states
Reachable states exploration and model construction done in 11.837 secs.
Sorting reachable states list...
Time for model construction: 12.179 seconds.
Type: CTMC
States: 119267 (1 initial)
Transitions: 1178621
---------------------------------------------------------------------
Verifying Lower Bound for change_state_min .....
---------------------------------------------------------------------
Model checking: "change_state_min": P=? [ F<=T ((EE>40&(!EE=-1))&(CC<20&(!CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 279.45 seconds.
Value in the initial state: 0.05427187832831769
Time for model checking: 279.472 seconds.
Result: 0.05427187832831769 (value in the initial state)
---------------------------------------------------------------------
Verifying Upper Bound for change_state_max .....
---------------------------------------------------------------------
Model checking: "change_state_max": P=? [ F<=T ((EE>40|(EE=-1))&(CC<20|(CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 279.425 seconds.
Value in the initial state: 0.054320821709538454
Time for model checking: 279.439 seconds.
Result: 0.054320821709538454 (value in the initial state)
========================================================================
Property: "change_state": P=? [ F<=T ((EE>40)&(CC<20)) ]
ProbMin: 0.05427187832831769 (value in the initial state)
ProbMax: 0.054320821709538454 (value in the initial state)
========================================================================